M.rframe(A.sends tfL of k on l)
== xdom((M.2.2.2.2.2.2.2.2.2.2).1). 

== L=(M.2.2.2.2.2.2.2.2.2.2).1(x)  
== L(deq-member(KindDeq;k;L))
==  (s1, s2:A.state, v:A.da(k).
==  (s1  s2 mod x)  (i:{0..||tfL||}. (tfL[i].2)(s1,v) = (tfL[i].2)(s2,v))) 

latex

---

clarification:

M.rframe(A.sends tfL of k on l)
== IdIdDeqxdom((M.2.2.2.2.2.2.2.2.2.2).1). 

== L=(M.2.2.2.2.2.2.2.2.2.2).1(x)  
== L(deq-member(KindDeq;k;L))
==  (s1:A.state, s2:A.state, v:A.da(k).
==  ma-x-equiv(A;x;s1;s2)
==   (i:{0..||tfL||}. (tfL[i].2)(s1,v) = (tfL[i].2)(s2,v)  (A.dout(l,tfL[i].1) List))) 

latex

Definitions	xdom(f). v=f(x)   P(x;v), Id, IdDeq, P  Q, b, deq-member(eq;x;L), KindDeq, M.state, M.da(a), P  Q, (s1  s2 mod x), x:A. B(x), {i..j}, #$n, ||as||, s = t, type List, M.dout(l,tg), t.1, f(a), t.2, l[i]
FDL editor aliases	ma-rframe-send